b:, x:Prop. if b x else False fi  b & x 

latex

Definitions	x:A. B(x), Prop, t  T, , Unit, b, True, P  Q, P  Q, P  Q, P & Q, False
Lemmas	false wf, true wf, bool wf